Makes use of the $$||_{\mathcal{A}}: \mathcal{A} \to \mathcal{A} \to \{ \textsf{false},\top \}$$ predicate we want to define for (abstract) digests to provide a sound basis for all of our MHP stuff for races and give a principled account of what I added in #518 .

Interestingly, it even does so outside of the context of data races --- which may be a cute insight on top of putting the race analysis on solid foundations with this predicate (and hopefully finding a way to get pthread_once to also fit (potentially in a reduced fashion)).

Technically, it accumulates the capacity and MHP information for all calls to wait for each barrier at a global unknown, and checks upon a call to wait that there are at least min(capacity)-1 other accesses where $$||_{\mathcal{A}}$$ is true pairwise among these, as well as with the caller to wait.

TODO:

• Use TIDs and Joins
• Use further abstract digests (such as must-lockset digest)
• Use information also for excluding races (beyond unreachability)
• Come up with a less expensive algorithm for checking there are min(capacity)-1 elements where $$||_{\mathcal{A}}$$ holds pairwise ?
• Handle barriers configured for inter-process communication soundly by not doing anything for them

Closes #1651.